Section: New Results

Combination of decision procedures

Participant : Pascal Fontaine.

We investigate the theoretical limits of combining decision procedures and reasoners, as these are important for the development of the veriT solver (see section  5.1 ). It has long been known that it is possible to extend any decidable language (subject to a minor requirement on cardinalities) with predicates described by a Bernays-Schönfinkel-Ramsey theory (BSR). A formula belongs to the BSR decidable fragment if it is a conjunction of universal, function-free formulas. As a consequence of this theoretical result, it is possible to extend a decidable quantifier-free language with sets and set operators, relations, orders and similar concepts. This can be used to significantly extend the expressivity of SMT solvers. In previous work, we had generalized this result to the decidable first-order class of monadic predicate logic, and to the two-variable fragment. In 2011, in cooperation with Carlos Areces from Universidad Nacional de Córdoba, Argentina, we showed that two other important decidable fragments (namely the Ackermann fragment, and several guarded fragments) are also easily combinable. This result was presented at the FroCoS Conference 2011 [8] , as well as at the SMT'2011 workshop (joint with the Conference on Computer Aided Verification, CAV 2011).